(DEFPROP INCLAUSES 
 (LAMBDA NIL
  (PROG (Z Z1 AXNO)
	(SETQ AXNO (QUOTE AXIOM))
   A    (SCANSET)
	(START)
	(SETQ ZIN (ERRSET (<INPUT>) T))
	(SCANRESET)
	(COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
	(SETQ ZIN (TOP))
	(COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z))
	      ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A))
	      ((MEMQ (CAR ZIN) DECOP) (GO B)))
	(OUT >S< ZIN)
	(SETQ Z
	      (APPEND Z
		      (SETUP
		       (CNF (COND ((EQ AXNO THEOREMNAME) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
	(GO A)
   B    (SETQ Z1 (CDR (ASSOC (CAR ZIN) DECTBL)))
	(COND ((EQ Z1 (QUOTE IVAR)) (MAKOVAR (SETQ IVAR (APPEND IVAR (CDR ZIN)))))
	      ((EQ Z1 (QUOTE EQUAL)) (SETQ PFLG NIL) (SETQ EQUAL (CADR ZIN)))
	      (T (SET Z1 (APPEND (CDR ZIN) (EVAL Z1)))))
	(OUT >INPUT< ZIN)
	(GO A))) 
EXPR)

(DEFPROP THEOREMNAME 
 (NIL . THEOREM) 
VALUE)